Flyspec Project
Kepler予想
の形式化のプロジェクト
HOL Light
で作られている？
Google Code Archive - Long-term storage for Google Code Project Hosting.
ここにあるリンクだと証明のコードをダウンロードできなかった
Webアーカイブで見ることが出来た日のページ:
Wayback Machine
おそらく現在はこっちで証明コードをダウンロードできる
Flyspeck I: Tame Graphs - Archive of Formal Proofs
#形式手法
#定理証明支援系